r,s:rationals. ((s = 0  rationals))  (qdiv(r; s)  rationals) 

latex

Definitions	prop{i:l}, qdiv(r; s), t  T, P  Q, x:A. B(x), P  Q, P  Q, P  Q, subtype(S; T)
Lemmas	assert-qeq, qeq wf2, assert wf, not functionality wrt iff, int inc rationals, rationals wf, not wf, qinv wf, qmul wf